Nuprl Lemma : ma-npre_wf
11,40
postcript
pdf
M
:MsgA,
a
:Id,
s
:
M
.state. unsolvable
M
.pre(
a
,
s
)
latex
Definitions
Id
,
t
T
,
x
:
A
.
B
(
x
)
,
State(
ds
)
,
x
:
A
B
(
x
)
,
,
x
.
A
(
x
)
,
x
.
t
(
x
)
,
a
:
A
fp
B
(
a
)
,
Top
,
P
Q
,
f
(
x
)
,
f
(
a
)
,
b
,
A
,
IdDeq
,
x
dom(
f
)
,
Type
,
,
z
!=
f
(
x
)
P
(
a
;
z
)
,
unsolvable
M
.pre(
a
,
s
)
,
M
.state
,
x
:
A
B
(
x
)
,
MsgA
Lemmas
fpf-dom
wf
,
id-deq
wf
,
not
wf
,
assert
wf
,
fpf-ap
wf
,
fpf-trivial-subtype-top
,
ma-state
wf
,
Id
wf
origin
M:MsgA, a:Id, s:M.state. unsolvable M.pre(a,s) 
M:MsgA, a:Id, s:M.state. unsolvable M.pre(a,s) Tx:A. B(x)
B(x)
x.A(x)
x. t(x) B(a)
Q
b
A dom(f) P(a;z)
B(x)